da1, da2:x:Knd fp Type. Normal(da1)  Normal(da2)  Normal(da1  da2) 

latex

Definitions	False, P  Q, A, left+right, P  Q, b, x:A. B(x), t  T, b, , s = t, Prop, Knd, Type, x.A(x), x. t(x), a:A fp B(a), Top, x:AB(x), KindDeq, x  dom(f), x:AB(x), P & Q, P  Q, Unit, Void, x:A. B(x), f  g, f(x), Normal(T), xdom(f). v=f(x)   P(x;v), Normal(da)
Lemmas	normal-da wf, fpf wf, fpf-join wf, top wf, fpf-join-ap-sq, fpf-join-dom, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, Kind-deq wf, fpf-trivial-subtype-top, Knd wf, bool wf, bnot wf, not wf, assert wf